1 /-
2 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro
5 -/
6 import data.rat.order
src └────────────┘
7 /-!
8 # Casts for Rational Numbers
9
10 ## Summary
11
12 We define the canonical injection from ℚ into an arbitrary division ring and prove various
13 casting lemmas showing the well-behavedness of this injection.
14
15 ## Notations
16
17 - `/.` is infix notation for `rat.mk`.
18
19 ## Tags
20
21 rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
22 -/
23
24 namespace rat
25 variable {α : Type*}
id ┴
typ ┴
26 open_locale rat
27
28 section with_div_ring
29 variable [division_ring α]
id └───────────┘
src └───────────┘
typ └───────────┘
30
31 /-- Construct the canonical injection from `ℚ` into an arbitrary
32 division ring. If the field has positive characteristic `p`,
33 we define `1 / p = 1 / 0 = 0` for consistency with our
34 division by zero convention. -/
35 protected def cast : ℚ → α
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc ┴
36 | ⟨n, d, h, c⟩ := n / d
id ┴ ┴ └┘ ┴
src └┘ ┴
typ ┴ ┴ └┘ ┴
37
38 @[priority 10] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩
id └─────┘ ┴ ┴ └──────┘
src └─────┘ ┴ └──────┘
typ └─────┘ ┴ ┴ └──────┘
doc ┴ └──────┘
39
40 @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n :=
id ┴ └────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴
doc └──┘ └────┘
41 show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ └─────┘
src ┴ ┴ ┴ └──┘└──────────┘└┘└─────┘└─
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└──────────┘└┘└─────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────┘└───────┘┴└
42
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
43 @[simp, squash_cast] theorem cast_coe_int (n : ℤ) : ((n : ℚ) : α) = n :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ ┴
44 by rw [coe_int_eq_of_int, cast_of_int]
id └───────────────┘ └─────────┘
src └──┘└───────────────┘└┘└─────────┘└─
typ └──┘└───────────────┘└┘└─────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────────┘└───────────┘┴└
45
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
46 @[simp, squash_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℚ) : α) = n := cast_coe_int n
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──┘ └─────────┘ ┴
47
48 @[simp, squash_cast] theorem cast_zero : ((0 : ℚ) : α) = 0 :=
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc └──┘ └─────────┘ ┴
49 (cast_of_int _).trans int.cast_zero
id └─────────┘ └───┘ └───────────┘
src └─────────┘ └───┘ └───────────┘
typ └─────────┘ └───┘ └───────────┘
50
51 @[simp, squash_cast] theorem cast_one : ((1 : ℚ) : α) = 1 :=
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc └──┘ └─────────┘ ┴
52 (cast_of_int _).trans int.cast_one
id └─────────┘ └───┘ └──────────┘
src └─────────┘ └───┘ └──────────┘
typ └─────────┘ └───┘ └──────────┘
53
54 theorem mul_cast_comm (a : α) :
id ┴
typ ┴
55 ∀ (n : ℚ), (n.denom : α) ≠ 0 → a * n = n * a
id ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
56 | ⟨n, d, h, c⟩ h₂ := show a * (n * d⁻¹) = n * d⁻¹ * a,
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
57 by rw [← mul_assoc, int.mul_cast_comm, mul_assoc, mul_assoc,
id └───────┘ └───────────────┘ └───────┘ └───────┘
src └────┘└───────┘└┘└───────────────┘└┘└───────┘└┘└───────┘└─
typ └────┘└───────┘└┘└───────────────┘└┘└───────┘└┘└───────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ └─
st └──────────────┘└─────────────────┘└─────────┘└─────────┘└─
58 ← show (d:α)⁻¹ * a = a * d⁻¹, from
id ┴ └┘ ┴ ┴
src ──────────┘ ┴ ┴ ┴└┘┴┴┴ ┴┴┴ ┴ ┴ └──────
typ ──────────┘ ┴ ┴┴┴└┘┴┴┴ ┴┴┴ ┴ ┴ └──────
doc ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
txt ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
par ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
pid ──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────
st ────────────────────────────────────────────
59 division_ring.inv_comm_of_comm h₂ (int.mul_cast_comm a d).symm]
id └────────────────────────────┘ └┘ └───────────────┘ ┴ ┴
src ──────────┘└────────────────────────────┘┴ ┴ └───────────────┘┴ ┴ └───────
typ ──────────┘└────────────────────────────┘┴└┘┴ └───────────────┘┴┴┴┴└───────
doc ──────────┘ ┴ ┴ ┴ ┴ └───────
txt ──────────┘ ┴ ┴ ┴ ┴ └───────
par ──────────┘ ┴ ┴ ┴ ┴ └───────
pid ──────────┘ ┴ ┴ ┴ ┴ └─────┘└
st ───────────────────────────────────────────────────────────────────────┘└┘└
60
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
61 @[move_cast] theorem cast_mk_of_ne_zero (a b : ℤ)
id ┴
src ┴
typ ┴
doc └───────┘
62 (b0 : (b:α) ≠ 0) : (a /. b : α) = a / b :=
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
63 begin
st └─────
64 have b0' : b ≠ 0, { refine mt _ b0, simp {contextual := tt} },
id ┴ ┴ └┘ └┘ └┘
src └─────────┘ ┴┴└┘ └─────┘└┘└─┘ └───┘ └────────────┘└┘└┘
typ └─────────┘┴┴┴└┘ └─────┘└┘└─┘└┘ └───┘ └────────────┘└┘└┘
doc └─────────┘ ┴ └┘ └─────┘ └─┘ └───┘ └────────────┘ └┘
txt └─────────┘ ┴ └┘ └─────┘ └─┘ └───┘ └────────────┘ └┘
par └─────────┘ ┴ └┘ └─────┘ └─┘ └───┘ └────────────┘ └┘
pid └──────┘└─┘ ┴ ┴┴ ┴ └─┘ ┴ └────────────┘ ┴┴
st ─────────────────┘└──┘└────────────┘└────────────────────────┘└┘└
65 cases e : a /. b with n d h c,
id ┴ ┴
src └────┘ └─┘ ┴ ┴ └───────────┘
typ └────┘ └─┘┴┴ ┴┴└───────────┘
doc └────┘ └─┘ ┴ ┴ └───────────┘
txt └────┘ └─┘ ┴ ┴ └───────────┘
par └────┘ └─┘ ┴ ┴ └───────────┘
pid ┴ └─┘ ┴ ┴ └───────────┘
st ──────────────────────────────┘└─
66 have d0 : (d:α) ≠ 0,
id ┴ ┴
src └────────┘ ┴ └┘ └┘
typ └────────┘ ┴┴┴└┘ └┘
doc └────────┘ ┴ └┘ └┘
txt └────────┘ ┴ └┘ └┘
par └────────┘ ┴ └┘ └┘
pid └─────┘└─┘ ┴ └┘ ┴┴
st ────────────────────┘└─
67 { intro d0,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ───┘└──────┘└─
68 have dd := denom_dvd a b,
id └───────┘ ┴ ┴
src └─────────┘└───────┘┴ ┴
typ └─────────┘└───────┘┴┴┴┴
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ───────────────────────────┘└─
69 cases (show (d:ℤ) ∣ b, by rwa e at dd) with k ke,
id ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ └┘┴┴ └───┘└──┘ └────┘└─────────┘
typ └────┘ ┴ ┴┴ └┘┴┴┴└───┘└──┘┴└────┘└─────────┘
doc └────┘ ┴ ┴ └┘ ┴ └───┘└──┘ └────┘└─────────┘
txt └────┘ ┴ ┴ └┘ ┴ └───┘└──┘ └────┘└─────────┘
par └────┘ ┴ ┴ └┘ ┴ └───┘└──┘ └────┘└─────────┘
pid ┴ ┴ ┴ └┘ ┴ └───────┘ └─────┘└────────┘
st ────────────────────────────┘└──────────┘└─────────┘└─
70 have : (b:α) = (d:α) * (k:α), {rw [ke, int.cast_mul], refl},
id ┴ ┴ ┴ ┴ ┴ └┘ └──────────┘
src └─────┘ ┴ └┘ ┴ ┴ └┘┴┴ ┴ ┴ └──┘ └┘└──────────┘┴ └──┘
typ └─────┘ ┴┴ └┘ ┴ ┴┴ └┘┴┴ ┴┴┴┴ └──┘└┘└┘└──────────┘┴ └──┘
doc └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ └──┘
txt └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ └──┘
par └─────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ └──┘
pid └───┘└┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴
st ───────────────────────────────┘└─────┘└┘└────────────┘└─────┘└┘└
71 rw [d0, zero_mul] at this, contradiction },
id └┘ └──────┘
src └──┘ └┘└──────┘└───────┘ └────────────┘
typ └──┘└┘└┘└──────┘└───────┘ └────────────┘
doc └──┘ └┘ └───────┘ └────────────┘
txt └──┘ └┘ └───────┘ └────────────┘
par └──┘ └┘ └───────┘ └────────────┘
pid └┘ └┘ ┴└──────┘ ┴
st ─────────┘└────────┘┴└──────┘└──────────────┘└┘└
72 rw [num_denom'] at e,
id └────────┘
src └──┘└────────┘└────┘
typ └──┘└────────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid └┘ ┴└───┘
st ───────────────┘┴└───┘└─
73 have := congr_arg (coe : ℤ → α) ((mk_eq b0' $ ne_of_gt $ int.coe_nat_pos.2 h).1 e),
id └───────┘ └─┘ ┴ └───┘ └─┘ └──────┘ └─────────────┘ ┴ ┴
src └──────┘└───────┘┴ └─┘└─┘ ┴ ┴ └┘ └───┘┴ ┴ ┴└──────┘┴ ┴└─────────────┘└─┘ └──┘ ┴
typ └──────┘└───────┘┴ └─┘└─┘ ┴ ┴┴└┘ └───┘┴└─┘┴ ┴└──────┘┴ ┴└─────────────┘└─┘┴└──┘┴┴
doc └──────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴
txt └──────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴
par └──────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴
pid └───┘└─┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
74 rw [int.cast_mul, int.cast_mul, int.cast_coe_nat] at this,
id └──────────┘ └──────────┘ └──────────────┘
src └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└───────┘
typ └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└───────┘
doc └──┘ └┘ └┘ └───────┘
txt └──┘ └┘ └┘ └───────┘
par └──┘ └┘ └┘ └───────┘
pid └┘ └┘ └┘ ┴└──────┘
st ─────────────────┘└────────────┘└────────────────┘┴└──────┘└─
75 symmetry, change (a * b⁻¹ : α) = n / d,
id ┴ ┴└┘ ┴ ┴ ┴ ┴
src └──────┘ └─────┘ ┴ ┴ └┘└─┘ └┘ ┴ ┴┴┴
typ └──────┘ └─────┘ ┴┴ ┴┴└┘└─┘┴└┘ ┴┴┴┴┴┴
doc └──────┘ └─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴
txt └──────┘ └─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴
par └──────┘ └─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴
st ─────────┘└────────────────────────────┘└─
76 rw [eq_div_iff_mul_eq _ _ d0, mul_assoc, nat.mul_cast_comm,
id └───────────────┘ └┘ └───────┘ └───────────────┘
src └──┘└───────────────┘└───┘ └┘└───────┘└┘└───────────────┘└─
typ └──┘└───────────────┘└───┘└┘└┘└───────┘└┘└───────────────┘└─
doc └──┘ └───┘ └┘ └┘ └─
txt └──┘ └───┘ └┘ └┘ └─
par └──┘ └───┘ └┘ └┘ └─
pid └┘ └───┘ └┘ └┘ └─
st ─────────────────────────────┘└─────────┘└─────────────────┘└─
77 ← mul_assoc, this, mul_assoc, mul_inv_cancel b0, mul_one]
id └───────┘ └──┘ └───────┘ └────────────┘ └┘ └─────┘
src ───────┘└───────┘└┘ └┘└───────┘└┘└────────────┘┴ └┘└─────┘└┘
typ ───────┘└───────┘└┘└──┘└┘└───────┘└┘└────────────┘┴└┘└┘└─────┘└┘
doc ───────┘ └┘ └┘ └┘ ┴ └┘ └┘
txt ───────┘ └┘ └┘ └┘ ┴ └┘ └┘
par ───────┘ └┘ └┘ └┘ ┴ └┘ └┘
pid ───────┘ └┘ └┘ └┘ ┴ └┘ ┴┴
st ────────────────┘└────┘└─────────┘└─────────────────┘└───────┘┴┴
78 end
st └─┘
79
80 @[move_cast] theorem cast_add_of_ne_zero : ∀ {m n : ℚ},
id ┴ ┴
src ┴
typ ┴ ┴
doc └───────┘ ┴
81 (m.denom : α) ≠ 0 → (n.denom : α) ≠ 0 → ((m + n : ℚ) : α) = m + n
id ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
82 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := λ (d₁0 : (d₁:α) ≠ 0) (d₂0 : (d₂:α) ≠ 0), begin
id └┘ └┘ ┴ ┴ ┴ ┴
src ┴ ┴
typ └┘ └┘ ┴ ┴ ┴ ┴
st └─────
83 have d₁0' : (d₁:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₁0; exact d₁0 rfl),
id └┘ ┴ ┴ └─────────────────┘ ┴ └─┘ └─┘
src └──────────┘ ┴┴└┘┴└────┘└─────────────────┘└─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴└─┘┴
typ └──────────┘ └┘┴┴└┘┴└────┘└─────────────────┘└─┘ └──┘ ┴└─┘┴└─────┘└┘└────┘└─┘┴└─┘┴
doc └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
txt └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
par └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
pid └───────┘└─┘ ┴ └┘ ┴└───┘ └─┘ └──┘ └──┘ └─────────────┘ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─────────────────────────┘┴└─
84 have d₂0' : (d₂:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₂0; exact d₂0 rfl),
id └┘ └─────────────────┘ ┴ └─┘ └─┘
src └──────────┘ ┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴└─┘┴
typ └──────────┘ └┘┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘┴└─────┘└┘└────┘└─┘┴└─┘┴
doc └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
txt └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
par └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
pid └───────┘└─┘ ┴ └┘ ┴└───┘ └─┘ └──┘ └──┘ └─────────────┘ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─────────────────────────┘┴└─
85 rw [num_denom', num_denom', add_def d₁0' d₂0'],
id └────────┘ └────────┘ └─────┘ └──┘ └──┘
src └──┘└────────┘└┘└────────┘└┘└─────┘┴ ┴ ┴
typ └──┘└────────┘└┘└────────┘└┘└─────┘┴└──┘┴└──┘┴
doc └──┘ └┘ └┘ ┴ ┴ ┴
txt └──┘ └┘ └┘ ┴ ┴ ┴
par └──┘ └┘ └┘ ┴ ┴ ┴
pid └┘ └┘ └┘ ┴ ┴ ┴
st ───────────────┘└──────────┘└─────────────────┘└──
86 suffices : (n₁ * (d₂ * (d₂⁻¹ * d₁⁻¹)) +
id ┴ └┘ ┴
src └─────────┘ ┴┴┴ ┴ ┴ └┘┴ ┴ └─┘┴└
typ └─────────┘ ┴┴┴ ┴ ┴ └┘┴ ┴ └─┘┴└
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid └───────┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ──────────────────────────────────────────
87 n₂ * (d₁ * d₂⁻¹) * d₁⁻¹ : α) = n₁ * d₁⁻¹ + n₂ * d₂⁻¹,
id ┴ ┴ └┘ └┘ └┘ └┘
src ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘┴└┘┴┴└┘┴ ┴└┘ ┴ ┴└┘┴ ┴└┘
doc ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
88 { rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero],
id └────────────────┘ └────────────────┘ └────────────────┘
src └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
typ └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───┘└────────────────────┘└──────────────────┘└──────────────────┘└──
89 { simpa [division_def, left_distrib, right_distrib, mul_inv_eq,
id └──────────┘ └──────────┘ └───────────┘ └────────┘
src └─────┘└──────────┘└┘└──────────┘└┘└───────────┘└┘└────────┘└─
typ └─────┘└──────────┘└┘└──────────┘└┘└───────────┘└┘└────────┘└─
doc └─────┘ └┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └─
st ─────┘└─────────────────────────────────────────────────────────────
90 d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0, mul_assoc] },
id └─┘ └─┘ └───────────────────────┘ └─┘ └─┘ └───────┘
src ────────────┘ └┘ └┘└───────────────────────┘┴ ┴ └┘└───────┘└┘
typ ────────────┘└─┘└┘└─┘└┘└───────────────────────┘┴└─┘┴└─┘└┘└───────┘└┘
doc ────────────┘ └┘ └┘ ┴ ┴ └┘ └┘
txt ────────────┘ └┘ └┘ ┴ ┴ └┘ └┘
par ────────────┘ └┘ └┘ ┴ ┴ └┘ └┘
pid ────────────┘ └┘ └┘ ┴ ┴ └┘ ┴┴
st ────────────────────────────────────────────────────────────────────┘└┘└
91 all_goals {simp [d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0]} },
id └─┘ └─┘ └───────────────────────┘ └─┘ └─┘
src └─────────┘└────┘ └┘ └┘└───────────────────────┘┴ ┴ ┴└┘
typ └─────────┘└────┘└─┘└┘└─┘└┘└───────────────────────┘┴└─┘┴└─┘┴└┘
doc └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
txt └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
par └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
pid └──────┘ └┘ └┘ ┴ ┴ └┘┴
st ──────────────┘└────────────────────────────────────────────────┘┴┴└┘└
92 rw [← mul_assoc (d₂:α), mul_inv_cancel d₂0, one_mul,
id └───────┘ └┘ ┴ └────────────┘ └─┘ └─────┘
src └────┘└───────┘┴ ┴ └─┘└────────────┘┴ └┘└─────┘└─
typ └────┘└───────┘┴ └┘┴┴└─┘└────────────┘┴└─┘└┘└─────┘└─
doc └────┘ ┴ ┴ └─┘ ┴ └┘ └─
txt └────┘ ┴ ┴ └─┘ ┴ └┘ └─
par └────┘ ┴ ┴ └─┘ ┴ └┘ └─
pid └──┘ ┴ ┴ └─┘ ┴ └┘ └─
st ───────────────────────┘└──────────────────┘└───────┘└─
93 ← nat.mul_cast_comm], simp [d₁0, mul_assoc]
id └───────────────┘ └─┘ └───────┘
src ───────┘└───────────────┘┴ └────┘ └┘└───────┘└┘
typ ───────┘└───────────────┘┴ └────┘└─┘└┘└───────┘└┘
doc ───────┘ ┴ └────┘ └┘ └┘
txt ───────┘ ┴ └────┘ └┘ └┘
par ───────┘ ┴ └────┘ └┘ └┘
pid ───────┘ ┴ ┴┴ └┘ ┴┴
st ────────────────────────┘└───────────────────────┘
94 end
st └─┘
95
96 @[simp, move_cast] theorem cast_neg : ∀ n, ((-n : ℚ) : α) = -n
id ┴ ┴┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴
doc └──┘ └───────┘ ┴
97 | ⟨n, d, h, c⟩ := show (↑-n * d⁻¹ : α) = -(n * d⁻¹),
id ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
src ┴┴ ┴ └┘ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
98 by rw [int.cast_neg, neg_mul_eq_neg_mul]
id └──────────┘ └────────────────┘
src └──┘└──────────┘└┘└────────────────┘└─
typ └──┘└──────────┘└┘└────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────┘└──────────────────┘┴└
99
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
100 @[move_cast] theorem cast_sub_of_ne_zero {m n : ℚ}
id ┴
src ┴
typ ┴
doc └───────┘ ┴
101 (m0 : (m.denom : α) ≠ 0) (n0 : (n.denom : α) ≠ 0) : ((m - n : ℚ) : α) = m - n :=
id ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
102 have ((-n).denom : α) ≠ 0, by cases n; exact n0,
id ┴┴ └───┘ ┴ ┴ ┴ └┘
src ┴ └───┘ ┴ └────┘ └────┘
typ ┴┴ └───┘ ┴ ┴ └────┘┴ └────┘└┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st └────────────────┘
103 by simp [(cast_add_of_ne_zero m0 this)]
id └─────────────────┘ └┘ └──┘
src └────┘ └─────────────────┘┴ ┴ └──
typ └────┘ └─────────────────┘┴└┘┴└──┘└──
doc └────┘ ┴ ┴ └──
txt └────┘ ┴ ┴ └──
par └────┘ ┴ ┴ └──
pid ┴┴ ┴ ┴ └┘└
st └─────────────────────────────────────
104
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
105 @[move_cast] theorem cast_mul_of_ne_zero : ∀ {m n : ℚ},
id ┴ ┴
src ┴
typ ┴ ┴
doc └───────┘ ┴
106 (m.denom : α) ≠ 0 → (n.denom : α) ≠ 0 → ((m * n : ℚ) : α) = m * n
id ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴└────┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
107 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := λ (d₁0 : (d₁:α) ≠ 0) (d₂0 : (d₂:α) ≠ 0), begin
id └┘ └┘ ┴ ┴ ┴ ┴
src ┴ ┴
typ └┘ └┘ ┴ ┴ ┴ ┴
st └─────
108 have d₁0' : (d₁:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₁0; exact d₁0 rfl),
id └┘ ┴ ┴ └─────────────────┘ ┴ └─┘ └─┘
src └──────────┘ ┴┴└┘┴└────┘└─────────────────┘└─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴└─┘┴
typ └──────────┘ └┘┴┴└┘┴└────┘└─────────────────┘└─┘ └──┘ ┴└─┘┴└─────┘└┘└────┘└─┘┴└─┘┴
doc └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
txt └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
par └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
pid └───────┘└─┘ ┴ └┘ ┴└───┘ └─┘ └──┘ └──┘ └─────────────┘ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─────────────────────────┘┴└─
109 have d₂0' : (d₂:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₂0; exact d₂0 rfl),
id └┘ └─────────────────┘ ┴ └─┘ └─┘
src └──────────┘ ┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴└─┘┴
typ └──────────┘ └┘┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘┴└─────┘└┘└────┘└─┘┴└─┘┴
doc └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
txt └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
par └──────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └─────┘└┘└────┘ ┴ ┴
pid └───────┘└─┘ ┴ └┘ ┴└───┘ └─┘ └──┘ └──┘ └─────────────┘ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─────────────────────────┘┴└─
110 rw [num_denom', num_denom', mul_def d₁0' d₂0'],
id └────────┘ └────────┘ └─────┘ └──┘ └──┘
src └──┘└────────┘└┘└────────┘└┘└─────┘┴ ┴ ┴
typ └──┘└────────┘└┘└────────┘└┘└─────┘┴└──┘┴└──┘┴
doc └──┘ └┘ └┘ ┴ ┴ ┴
txt └──┘ └┘ └┘ ┴ ┴ ┴
par └──┘ └┘ └┘ ┴ ┴ ┴
pid └┘ └┘ └┘ ┴ ┴ ┴
st ───────────────┘└──────────┘└─────────────────┘└──
111 suffices : (n₁ * ((n₂ * d₂⁻¹) * d₁⁻¹) : α) = n₁ * (d₁⁻¹ * (n₂ * d₂⁻¹)),
id ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘
src └─────────┘ ┴┴┴ ┴ ┴ └┘└┘ ┴ └──┘ └┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ └─────────┘ ┴┴┴ ┴ ┴ └┘└┘ ┴ └──┘┴└┘┴┴└┘┴ ┴ └┘ ┴ ┴ └┘┴ ┴└┘ └┘
doc └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───────┘└┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────┘└─
112 { rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero],
id └────────────────┘ └────────────────┘ └────────────────┘
src └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
typ └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───┘└────────────────────┘└──────────────────┘└──────────────────┘└──
113 { simpa [division_def, mul_inv_eq, d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0, mul_assoc] },
id └──────────┘ └────────┘ └─┘ └─┘ └───────────────────────┘ └─┘ └─┘ └───────┘
src └─────┘└──────────┘└┘└────────┘└┘ └┘ └┘└───────────────────────┘┴ ┴ └┘└───────┘└┘
typ └─────┘└──────────┘└┘└────────┘└┘└─┘└┘└─┘└┘└───────────────────────┘┴└─┘┴└─┘└┘└───────┘└┘
doc └─────┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘
txt └─────┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘
par └─────┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘
pid ┴┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴┴
st ─────┘└───────────────────────────────────────────────────────────────────────────────────────┘└┘└
114 all_goals {simp [d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0]} },
id └─┘ └─┘ └───────────────────────┘ └─┘ └─┘
src └─────────┘└────┘ └┘ └┘└───────────────────────┘┴ ┴ ┴└┘
typ └─────────┘└────┘└─┘└┘└─┘└┘└───────────────────────┘┴└─┘┴└─┘┴└┘
doc └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
txt └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
par └─────────┘└────┘ └┘ └┘ ┴ ┴ ┴└┘
pid └──────┘ └┘ └┘ ┴ ┴ └┘┴
st ──────────────┘└────────────────────────────────────────────────┘┴┴└┘└
115 rw [division_ring.inv_comm_of_comm d₁0 (nat.mul_cast_comm _ _).symm]
id └────────────────────────────┘ └─┘ └───────────────┘
src └──┘└────────────────────────────┘┴ ┴ └───────────────┘└──────────┘
typ └──┘└────────────────────────────┘┴└─┘┴ └───────────────┘└──────────┘
doc └──┘ ┴ ┴ └──────────┘
txt └──┘ ┴ ┴ └──────────┘
par └──┘ ┴ ┴ └──────────┘
pid └┘ ┴ ┴ └─────────┘┴
st ───────────────────────────────────────────────────────────────────┘└┘┴
116 end
st └─┘
117
118 @[move_cast] theorem cast_inv_of_ne_zero : ∀ {n : ℚ},
id ┴ ┴
src ┴
typ ┴ ┴
doc └───────┘ ┴
119 (n.num : α) ≠ 0 → (n.denom : α) ≠ 0 → ((n⁻¹ : ℚ) : α) = n⁻¹
id ┴└──┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
src └──┘ ┴ └────┘ ┴ └┘ ┴ ┴ └┘
typ ┴└──┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
doc ┴
120 | ⟨n, d, h, c⟩ := λ (n0 : (n:α) ≠ 0) (d0 : (d:α) ≠ 0), begin
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st └─────
121 have n0' : (n:ℤ) ≠ 0 := λ e, by rw e at n0; exact n0 rfl,
id ┴ ┴ ┴ └┘ └─┘
src └─────────┘ ┴ └┘┴└────┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴└─┘
typ └─────────┘ ┴┴ └┘┴└────┘ └──┘ ┴└─┘┴└────┘└┘└────┘└┘┴└─┘
doc └─────────┘ ┴ └┘ └────┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴
txt └─────────┘ ┴ └┘ └────┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴
par └─────────┘ ┴ └┘ └────┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴
pid └──────┘└─┘ ┴ └┘ ┴└───┘ └──┘ └──┘ └────────────┘ ┴
st ────────────────────────────────┘└───────────────────────┘└─
122 have d0' : (d:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d0; exact d0 rfl),
id ┴ └─────────────────┘ ┴ └┘ └─┘
src └─────────┘ ┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴└─┘┴
typ └─────────┘ ┴┴ └┘ └────┘└─────────────────┘└─┘ └──┘ ┴└─┘┴└────┘└┘└────┘└┘┴└─┘┴
doc └─────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴ ┴
txt └─────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴ ┴
par └─────────┘ ┴ └┘ └────┘ └─┘ └──┘ ┴└─┘ └────┘└┘└────┘ ┴ ┴
pid └──────┘└─┘ ┴ └┘ ┴└───┘ └─┘ └──┘ └──┘ └────────────┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└───────────────────────┘┴└─
123 rw [num_denom', inv_def],
id └────────┘ └─────┘
src └──┘└────────┘└┘└─────┘┴
typ └──┘└────────┘└┘└─────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────┘└───────┘└──
124 rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, inv_div];
id └────────────────┘ └────────────────┘ └─────┘
src └──┘└────────────────┘└┘└────────────────┘└┘└─────┘┴
typ └──┘└────────────────┘└┘└────────────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────────────────────┘└──────────────────┘└───────┘┴└─
125 simp [n0, d0]
id └┘ └┘
src └────┘ └┘ └┘
typ └────┘└┘└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────┘
126 end
st └─┘
127
128 @[move_cast] theorem cast_div_of_ne_zero {m n : ℚ} (md : (m.denom : α) ≠ 0)
id ┴ ┴└────┘ ┴ ┴
src ┴ └────┘ ┴
typ ┴ ┴└────┘ ┴ ┴
doc └───────┘ ┴
129 (nn : (n.num : α) ≠ 0) (nd : (n.denom : α) ≠ 0) : ((m / n : ℚ) : α) = m / n :=
id ┴└──┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴└──┘ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
130 have (n⁻¹.denom : ℤ) ∣ n.num,
id ┴└┘└───┘ ┴ ┴ ┴└──┘
src └┘└───┘ ┴ ┴ └──┘
typ ┴└┘└───┘ ┴ ┴ ┴└──┘
131 by conv in n⁻¹.denom { rw [←(@num_denom n), inv_def] };
id ┴└┘ └───────┘ ┴ └─────┘
src └──────┘ └┘└───────┘└───┘ └───────┘┴ └─┘└─────┘└┘┴
typ └──────┘┴└┘└───────┘└───┘ └───────┘┴┴└─┘└─────┘└┘┴
txt └──────┘ └───────┘└───┘ ┴ └─┘ └┘┴
par └──────┘ └───────┘└───┘ ┴ └─┘ └┘┴
pid ┴└─┘ └───┘└───────┘ ┴ └─┘ └─┘
st └──────────────────┘└──────────────────┘└───────┘ ┴└┘└
132 apply denom_dvd,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────┘
133 have (n⁻¹.denom : α) = 0 → (n.num : α) = 0, from
id ┴└┘└───┘ ┴ ┴ ┴└──┘ ┴ ┴
src └┘└───┘ ┴ └──┘ ┴
typ ┴└┘└───┘ ┴ ┴ ┴└──┘ ┴ ┴
134 λ h, let ⟨k, e⟩ := this in
id ┴ └─┘ └──┘
typ ┴ └─┘ └──┘
135 by have := congr_arg (coe : ℤ → α) e;
id └───────┘ └─┘ ┴ ┴
src └──────┘└───────┘┴ └─┘└─┘ ┴ ┴ └┘
typ └──────┘└───────┘┴ └─┘└─┘ ┴ ┴┴└┘┴
doc └──────┘ ┴ └─┘ ┴ ┴ └┘
txt └──────┘ ┴ └─┘ ┴ ┴ └┘
par └──────┘ ┴ └─┘ ┴ ┴ └┘
pid └───┘└─┘ ┴ └─┘ ┴ ┴ └┘
st └───────────────────────────────────
136 rwa [int.cast_mul, int.cast_coe_nat, h, zero_mul] at this,
id └──────────┘ └──────────────┘ ┴ └──────┘
src └───┘└──────────┘└┘└──────────────┘└┘ └┘└──────┘└───────┘
typ └───┘└──────────┘└┘└──────────────┘└┘┴└┘└──────┘└───────┘
doc └───┘ └┘ └┘ └┘ └───────┘
txt └───┘ └┘ └┘ └┘ └───────┘
par └───┘ └┘ └┘ └┘ └───────┘
pid └┘ └┘ └┘ └┘ ┴└──────┘
st ─────────┘└──────────┘└────────────────┘└─┘└────────┘┴└──────┘
137 by rw [division_def, cast_mul_of_ne_zero md (mt this nn), cast_inv_of_ne_zero nn nd, division_def]
id └──────────┘ └─────────────────┘ └┘ └┘ └──┘ └┘ └─────────────────┘ └┘ └┘ └──────────┘
src └──┘└──────────┘└┘└─────────────────┘┴ ┴ └┘┴ ┴ └─┘└─────────────────┘┴ ┴ └┘└──────────┘└─
typ └──┘└──────────┘└┘└─────────────────┘┴└┘┴ └┘┴└──┘┴└┘└─┘└─────────────────┘┴└┘┴└┘└┘└──────────┘└─
doc └──┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ └─
txt └──┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ └─
par └──┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ └─
pid └┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴└
st └───────────────┘└───────────────────────────────────┘└─────────────────────────┘└────────────┘┴└
138
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
139 @[simp, elim_cast] theorem cast_inj [char_zero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ └───────┘ ┴
140 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := begin
st └─────
141 refine ⟨λ h, _, congr_arg _⟩,
id └───────┘
src └─────┘ └─────┘└───────┘└─┘
typ └─────┘ └─────┘└───────┘└─┘
doc └─────┘ └─────┘ └─┘
txt └─────┘ └─────┘ └─┘
par └─────┘ └─────┘ └─┘
pid ┴ └─────┘ └─┘
st ─────────────────────────────┘└─
142 have d₁0 : d₁ ≠ 0 := ne_of_gt h₁,
id └┘ ┴ └──────┘ └┘
src └─────────┘ ┴┴└────┘└──────┘┴
typ └─────────┘└┘┴┴└────┘└──────┘┴└┘
doc └─────────┘ ┴ └────┘ ┴
txt └─────────┘ ┴ └────┘ ┴
par └─────────┘ ┴ └────┘ ┴
pid └──────┘└─┘ ┴ ┴└───┘ ┴
st ─────────────────────────────────┘└─
143 have d₂0 : d₂ ≠ 0 := ne_of_gt h₂,
id └┘ └──────┘ └┘
src └─────────┘ ┴ └────┘└──────┘┴
typ └─────────┘└┘┴ └────┘└──────┘┴└┘
doc └─────────┘ ┴ └────┘ ┴
txt └─────────┘ ┴ └────┘ ┴
par └─────────┘ ┴ └────┘ ┴
pid └──────┘└─┘ ┴ ┴└───┘ ┴
st ─────────────────────────────────┘└─
144 have d₁a : (d₁:α) ≠ 0 := nat.cast_ne_zero.2 d₁0,
id └┘ ┴ └──────────────┘ └─┘
src └─────────┘ ┴ └┘ └────┘└──────────────┘└─┘
typ └─────────┘ └┘┴┴└┘ └────┘└──────────────┘└─┘└─┘
doc └─────────┘ ┴ └┘ └────┘ └─┘
txt └─────────┘ ┴ └┘ └────┘ └─┘
par └─────────┘ ┴ └┘ └────┘ └─┘
pid └──────┘└─┘ ┴ └┘ ┴└───┘ └─┘
st ────────────────────────────────────────────────┘└─
145 have d₂a : (d₂:α) ≠ 0 := nat.cast_ne_zero.2 d₂0,
id └┘ ┴ └──────────────┘ └─┘
src └─────────┘ ┴ └┘ └────┘└──────────────┘└─┘
typ └─────────┘ └┘┴┴└┘ └────┘└──────────────┘└─┘└─┘
doc └─────────┘ ┴ └┘ └────┘ └─┘
txt └─────────┘ ┴ └┘ └────┘ └─┘
par └─────────┘ ┴ └┘ └────┘ └─┘
pid └──────┘└─┘ ┴ └┘ ┴└───┘ └─┘
st ────────────────────────────────────────────────┘└─
146 rw [num_denom', num_denom'] at h ⊢,
id └────────┘ └────────┘
src └──┘└────────┘└┘└────────┘└──────┘
typ └──┘└────────┘└┘└────────┘└──────┘
doc └──┘ └┘ └──────┘
txt └──┘ └┘ └──────┘
par └──┘ └┘ └──────┘
pid └┘ └┘ ┴└─────┘
st ───────────────┘└──────────┘┴└─────┘└─
147 rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h; simp [d₁0, d₂0] at h ⊢,
id └────────────────┘ └────────────────┘ └─┘ └─┘
src └──┘└────────────────┘└┘└────────────────┘└────┘ └────┘ └┘ └──────┘
typ └──┘└────────────────┘└┘└────────────────┘└────┘ └────┘└─┘└┘└─┘└──────┘
doc └──┘ └┘ └────┘ └────┘ └┘ └──────┘
txt └──┘ └┘ └────┘ └────┘ └┘ └──────┘
par └──┘ └┘ └────┘ └────┘ └┘ └──────┘
pid └┘ └┘ ┴└───┘ ┴┴ └┘ ┴┴└────┘
st ───────────────────────┘└──────────────────┘┴└───────────────────────────┘└─
148 rwa [eq_div_iff_mul_eq _ _ d₂a, division_def, mul_assoc,
id └───────────────┘ └─┘ └──────────┘ └───────┘
src └───┘└───────────────┘└───┘ └┘└──────────┘└┘└───────┘└─
typ └───┘└───────────────┘└───┘└─┘└┘└──────────┘└┘└───────┘└─
doc └───┘ └───┘ └┘ └┘ └─
txt └───┘ └───┘ └┘ └┘ └─
par └───┘ └───┘ └┘ └┘ └─
pid └┘ └───┘ └┘ └┘ └─
st ───────────────────────────────┘└────────────┘└─────────┘└─
149 division_ring.inv_comm_of_comm d₁a (nat.mul_cast_comm _ _),
id └────────────────────────────┘ └─┘ └───────────────┘
src ───┘└────────────────────────────┘┴ ┴ └───────────────┘└──────
typ ───┘└────────────────────────────┘┴└─┘┴ └───────────────┘└──────
doc ───┘ ┴ ┴ └──────
txt ───┘ ┴ ┴ └──────
par ───┘ ┴ ┴ └──────
pid ───┘ ┴ ┴ └──────
st ─────────────────────────────────────────────────────────────┘└─
150 ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq _ _ d₁a, eq_comm,
id └───────┘ └──────────┘ └─────┘ └───────────────┘ └─┘ └─────┘
src ─────┘└───────┘└──┘└──────────┘└┘└─────┘└┘└───────────────┘└───┘ └┘└─────┘└─
typ ─────┘└───────┘└──┘└──────────┘└┘└─────┘└┘└───────────────┘└───┘└─┘└┘└─────┘└─
doc ─────┘ └──┘ └┘ └┘ └───┘ └┘ └─
txt ─────┘ └──┘ └┘ └┘ └───┘ └┘ └─
par ─────┘ └──┘ └┘ └┘ └───┘ └┘ └─
pid ─────┘ └──┘ └┘ └┘ └───┘ └┘ └─
st ──────────────┘└──────────────┘└───────┘└─────────────────────────┘└───────┘└─
151 ← int.cast_coe_nat, ← int.cast_mul, ← int.cast_coe_nat, ← int.cast_mul,
id └──────────────┘ └──────────┘ └──────────────┘ └──────────┘
src ─────┘└──────────────┘└──┘└──────────┘└──┘└──────────────┘└──┘└──────────┘└─
typ ─────┘└──────────────┘└──┘└──────────┘└──┘└──────────────┘└──┘└──────────┘└─
doc ─────┘ └──┘ └──┘ └──┘ └─
txt ─────┘ └──┘ └──┘ └──┘ └─
par ─────┘ └──┘ └──┘ └──┘ └─
pid ─────┘ └──┘ └──┘ └──┘ └─
st ─────────────────────┘└──────────────┘└──────────────────┘└──────────────┘└─
152 int.cast_inj, ← mk_eq (int.coe_nat_ne_zero.2 d₁0) (int.coe_nat_ne_zero.2 d₂0)] at h
id └──────────┘ └───┘ └─┘ └─────────────────┘ └─┘
src ───┘└──────────┘└──┘└───┘┴ └─┘ └┘ └─────────────────┘└─┘ └──────┘
typ ───┘└──────────┘└──┘└───┘┴ └─┘└─┘└┘ └─────────────────┘└─┘└─┘└──────┘
doc ───┘ └──┘ ┴ └─┘ └┘ └─┘ └──────┘
txt ───┘ └──┘ ┴ └─┘ └┘ └─┘ └──────┘
par ───┘ └──┘ ┴ └─┘ └┘ └─┘ └──────┘
pid ───┘ └──┘ ┴ └─┘ └┘ └─┘ └┘└───┘┴
st ───────────────┘└───────────────────────────────────────────────────────────────┘┴└────┘
153 end
st └─┘
154
155 theorem cast_injective [char_zero α] : function.injective (coe : ℚ → α)
id └───────┘ ┴ └────────────────┘ └─┘ ┴ ┴
src └───────┘ └────────────────┘ └─┘ ┴
typ └───────┘ ┴ └────────────────┘ └─┘ ┴ ┴
doc └───────┘ ┴
156 | m n := cast_inj.1
id └──────┘┴
src └──────┘┴
typ └──────┘┴
157
158 @[simp] theorem cast_eq_zero [char_zero α] {n : ℚ} : (n : α) = 0 ↔ n = 0 :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ ┴
159 by rw [← cast_zero, cast_inj]
id └───────┘ └──────┘
src └────┘└───────┘└┘└──────┘└─
typ └────┘└───────┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └──────────────┘└────────┘┴└
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 @[simp] theorem cast_ne_zero [char_zero α] {n : ℚ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ ┴
162 not_congr cast_eq_zero
id └───────┘ └──────────┘
src └───────┘ └──────────┘
typ └───────┘ └──────────┘
163
164 theorem eq_cast_of_ne_zero (f : ℚ → α) (H1 : f 1 = 1)
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴
165 (Hadd : ∀ x y, f (x + y) = f x + f y)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
166 (Hmul : ∀ x y, f (x * y) = f x * f y) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
167 ∀ n : ℚ, (n.denom : α) ≠ 0 → f n = n
id ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ ┴
typ ┴ ┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
168 | ⟨n, d, h, c⟩ := λ (h₂ : ((d:ℤ):α) ≠ 0), show _ = (n / (d:ℤ) : α), begin
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └─────
169 rw [num_denom', mk_eq_div, eq_div_iff_mul_eq _ _ h₂],
id └────────┘ └───────┘ └───────────────┘ └┘
src └──┘└────────┘└┘└───────┘└┘└───────────────┘└───┘ ┴
typ └──┘└────────┘└┘└───────┘└┘└───────────────┘└───┘└┘┴
doc └──┘ └┘ └┘ └───┘ ┴
txt └──┘ └┘ └┘ └───┘ ┴
par └──┘ └┘ └┘ └───┘ ┴
pid └┘ └┘ └┘ └───┘ ┴
st ───────────────┘└─────────┘└────────────────────────┘└──
170 have : ∀ n : ℤ, f n = n, { apply int.eq_cast; simp [H1, Hadd] },
id ┴ ┴ └─────────┘ └┘ └──┘
src └─────┘ └───┘ ┴ ┴ ┴┴┴ └────┘└─────────┘ └────┘ └┘ └┘
typ └─────┘ └───┘ ┴┴┴ ┴┴┴ └────┘└─────────┘ └────┘└┘└┘└──┘└┘
doc └─────┘ └───┘ ┴ ┴ ┴ ┴ └────┘ └────┘ └┘ └┘
txt └─────┘ └───┘ ┴ ┴ ┴ ┴ └────┘ └────┘ └┘ └┘
par └─────┘ └───┘ ┴ ┴ ┴ ┴ └────┘ └────┘ └┘ └┘
pid └───┘└┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴┴
st ────────────────────────┘└──┘└─────────────────────────────────┘└┘└
171 rw [← this, ← this, ← Hmul, div_mul_cancel],
id └──┘ └──┘ └──┘ └────────────┘
src └────┘ └──┘ └──┘ └┘└────────────┘┴
typ └────┘└──┘└──┘└──┘└──┘└──┘└┘└────────────┘┴
doc └────┘ └──┘ └──┘ └┘ ┴
txt └────┘ └──┘ └──┘ └┘ ┴
par └────┘ └──┘ └──┘ └┘ ┴
pid └──┘ └──┘ └──┘ └┘ ┴
st ───────────┘└──────┘└──────┘└──────────────┘└──
172 exact int.cast_ne_zero.2 (int.coe_nat_ne_zero.2 $ ne_of_gt h),
id └──────────────┘ └─────────────────┘ └──────┘ ┴
src └────┘└──────────────┘└─┘ └─────────────────┘└─┘ ┴└──────┘┴ ┴
typ └────┘└──────────────┘└─┘ └─────────────────┘└─┘ ┴└──────┘┴┴┴
doc └────┘ └─┘ └─┘ ┴ ┴ ┴
txt └────┘ └─┘ └─┘ ┴ ┴ ┴
par └────┘ └─┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
173 end
st ──┘
174
175 theorem eq_cast [char_zero α] (f : ℚ → α) (H1 : f 1 = 1)
id └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴
176 (Hadd : ∀ x y, f (x + y) = f x + f y)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
177 (Hmul : ∀ x y, f (x * y) = f x * f y) (n : ℚ) : f n = n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
178 eq_cast_of_ne_zero _ H1 Hadd Hmul _ $
id └────────────────┘ └┘ └──┘ └──┘
src └────────────────┘
typ └────────────────┘ └┘ └──┘ └──┘
179 nat.cast_ne_zero.2 $ ne_of_gt n.pos
id └──────────────┘┴ └──────┘ ┴└──┘
src └──────────────┘┴ └──────┘ └──┘
typ └──────────────┘┴ └──────┘ ┴└──┘
180
181 @[simp, move_cast] theorem cast_add [char_zero α] (m n) :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └──┘ └───────┘ └───────┘
182 ((m + n : ℚ) : α) = m + n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
183 cast_add_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
src └─────────────────┘ └──────────────┘┴ └──────┘ └──┘ └──────────────┘┴ └──────┘ └──┘
typ └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
184
185 @[simp, move_cast] theorem cast_sub [char_zero α] (m n) :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └──┘ └───────┘ └───────┘
186 ((m - n : ℚ) : α) = m - n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
187 cast_sub_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
src └─────────────────┘ └──────────────┘┴ └──────┘ └──┘ └──────────────┘┴ └──────┘ └──┘
typ └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
188
189 @[simp, move_cast] theorem cast_mul [char_zero α] (m n) :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └──┘ └───────┘ └───────┘
190 ((m * n : ℚ) : α) = m * n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
191 cast_mul_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
src └─────────────────┘ └──────────────┘┴ └──────┘ └──┘ └──────────────┘┴ └──────┘ └──┘
typ └─────────────────┘ └──────────────┘┴ └──────┘ ┴└──┘ └──────────────┘┴ └──────┘ ┴└──┘
192
193 @[simp, squash_cast, move_cast] theorem cast_bit0 [char_zero α] (n : ℚ) :
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └──┘ └─────────┘ └───────┘ └───────┘ ┴
194 ((bit0 n : ℚ) : α) = bit0 n :=
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴
doc ┴
195 cast_add _ _
id └──────┘
src └──────┘
typ └──────┘
196
197 @[simp, squash_cast, move_cast] theorem cast_bit1 [char_zero α] (n : ℚ) :
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └──┘ └─────────┘ └───────┘ └───────┘ ┴
198 ((bit1 n : ℚ) : α) = bit1 n :=
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴
doc ┴
199 by rw [bit1, cast_add, cast_one, cast_bit0]; refl
id └──┘ └──────┘ └──────┘ └───────┘
src └──┘└──┘└┘└──────┘└┘└──────┘└┘└───────┘┴ └────
typ └──┘└──┘└┘└──────┘└┘└──────┘└┘└───────┘┴ └────
doc └──┘ └┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ ┴ └
st └───────┘└────────┘└────────┘└─────────┘┴└──────
200
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
201 instance is_ring_hom_cast [char_zero α] : is_ring_hom (rat.cast : ℚ → α) :=
id └───────┘ ┴ └─────────┘ └──────┘ ┴ ┴
src └───────┘ └─────────┘ └──────┘ ┴
typ └───────┘ ┴ └─────────┘ └──────┘ ┴ ┴
doc └───────┘ └─────────┘ └──────┘ ┴
202 ⟨rat.cast_one, rat.cast_mul, rat.cast_add⟩
id └──────────┘ └──────────┘ └──────────┘
src └──────────┘ └──────────┘ └──────────┘
typ └──────────┘ └──────────┘ └──────────┘
203
204 end with_div_ring
205
206 @[move_cast] theorem cast_mk [discrete_field α] [char_zero α] (a b : ℤ) : ((a /. b) : α) = a / b :=
id └────────────┘ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └───────┘ ┴ └┘ ┴ ┴
typ └────────────┘ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘ └┘
207 if b0 : b = 0 then by simp [b0, div_zero]
id └┘ ┴ ┴ └┘ └──────┘
src └┘ ┴ └────┘ └┘└──────┘└┘
typ └┘ ┴ ┴ └────┘└┘└┘└──────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └───────────────────┘
208 else cast_mk_of_ne_zero a b (int.cast_ne_zero.2 b0)
id └────────────────┘ ┴ ┴ └──────────────┘┴ └┘
src └────────────────┘ └──────────────┘┴
typ └────────────────┘ ┴ ┴ └──────────────┘┴ └┘
209
210 @[simp, move_cast] theorem cast_inv [discrete_field α] [char_zero α] (n) : ((n⁻¹ : ℚ) : α) = n⁻¹ :=
id └────────────┘ ┴ └───────┘ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
src └────────────┘ └───────┘ └┘ ┴ ┴ └┘
typ └────────────┘ ┴ └───────┘ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
doc └──┘ └───────┘ └───────┘ ┴
211 if n0 : n.num = 0 then
id └┘ ┴└──┘ ┴
src └┘ └──┘ ┴
typ └┘ ┴└──┘ ┴
212 by simp [show n = 0, by rw [←(@num_denom n), n0]; simp, inv_zero] else
id ┴ ┴ └───────┘ ┴ └┘ └──────┘
src └────┘ ┴ ┴┴└─────┘└───┘ └───────┘┴ └─┘ ┴└──────┘└──────┘└┘
typ └────┘ ┴┴┴┴└─────┘└───┘ └───────┘┴┴└─┘└┘┴└──────┘└──────┘└┘
doc └────┘ ┴ ┴ └─────┘└───┘ ┴ └─┘ ┴└──────┘ └┘
txt └────┘ ┴ ┴ └─────┘└───┘ ┴ └─┘ ┴└──────┘ └┘
par └────┘ ┴ ┴ └─────┘└───┘ ┴ └─┘ ┴└──────┘ └┘
pid ┴┴ ┴ ┴ └──────────┘ ┴ └─┘ └───────┘ ┴┴
st └───────────────────┘└──────────────────┘└──┘┴└────┘└──────────┘
213 cast_inv_of_ne_zero (int.cast_ne_zero.2 n0) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id └─────────────────┘ └──────────────┘┴ └┘ └──────────────┘┴ └──────┘ ┴└──┘
src └─────────────────┘ └──────────────┘┴ └──────────────┘┴ └──────┘ └──┘
typ └─────────────────┘ └──────────────┘┴ └┘ └──────────────┘┴ └──────┘ ┴└──┘
214
215 @[simp, move_cast] theorem cast_div [discrete_field α] [char_zero α] (m n) :
id └────────────┘ ┴ └───────┘ ┴
src └────────────┘ └───────┘
typ └────────────┘ ┴ └───────┘ ┴
doc └──┘ └───────┘ └───────┘
216 ((m / n : ℚ) : α) = m / n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
217 by rw [division_def, cast_mul, cast_inv, division_def]
id └──────────┘ └──────┘ └──────┘ └──────────┘
src └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
typ └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └───────────────┘└────────┘└────────┘└────────────┘┴└
218
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
219 @[simp, move_cast] theorem cast_pow [discrete_field α] [char_zero α] (q) (k : ℕ) :
id └────────────┘ ┴ └───────┘ ┴ ┴
src └────────────┘ └───────┘ ┴
typ └────────────┘ ┴ └───────┘ ┴ ┴
doc └──┘ └───────┘ └───────┘
220 ((q ^ k : ℚ) : α) = q ^ k :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
221 by induction k; simp only [*, cast_one, cast_mul, pow_zero, pow_succ]
id ┴ └──────┘ └──────┘ └──────┘ └──────┘
src └────────┘ └────────────┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
typ └────────┘┴ └────────────┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
doc └────────┘ └────────────┘ └┘ └┘ └┘ └─
txt └────────┘ └────────────┘ └┘ └┘ └┘ └─
par └────────┘ └────────────┘ └┘ └┘ └┘ └─
pid ┴ ┴└──┘└───┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────
222
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
223 @[simp] theorem cast_nonneg [linear_ordered_field α] : ∀ {n : ℚ}, 0 ≤ (n : α) ↔ 0 ≤ n
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
224 | ⟨n, d, h, c⟩ := show 0 ≤ (n * d⁻¹ : α) ↔ 0 ≤ (⟨n, d, h, c⟩ : ℚ),
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc ┴
225 by rw [num_denom', ← nonneg_iff_zero_le, mk_nonneg _ (int.coe_nat_pos.2 h),
id └────────┘ └────────────────┘ └───────┘ └─────────────┘ ┴
src └──┘└────────┘└──┘└────────────────┘└┘└───────┘└─┘ └─────────────┘└─┘ └──
typ └──┘└────────┘└──┘└────────────────┘└┘└───────┘└─┘ └─────────────┘└─┘┴└──
doc └──┘ └──┘ └┘ └─┘ └─┘ └──
txt └──┘ └──┘ └┘ └─┘ └─┘ └──
par └──┘ └──┘ └┘ └─┘ └─┘ └──
pid └┘ └──┘ └┘ └─┘ └─┘ └──
st └─────────────┘└────────────────────┘└─────────────────────────────────┘└─
226 mul_nonneg_iff_right_nonneg_of_pos (@inv_pos α _ _ (nat.cast_pos.2 h)),
id └────────────────────────────────┘ └─────┘ ┴ └──────────┘ ┴
src ───┘└────────────────────────────────┘┴ └─────┘┴ └───┘ └──────────┘└─┘ └───
typ ───┘└────────────────────────────────┘┴ └─────┘┴┴└───┘ └──────────┘└─┘┴└───
doc ───┘ ┴ ┴ └───┘ └─┘ └───
txt ───┘ ┴ ┴ └───┘ └─┘ └───
par ───┘ ┴ ┴ └───┘ └─┘ └───
pid ───┘ ┴ ┴ └───┘ └─┘ └───
st ─────────────────────────────────────────────────────────────────────────┘└─
227 int.cast_nonneg]
id └─────────────┘
src ───┘└─────────────┘└─
typ ───┘└─────────────┘└─
doc ───┘ └─
txt ───┘ └─
par ───┘ └─
pid ───┘ ┴└
st ──────────────────┘┴└
228
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
229 @[simp, elim_cast] theorem cast_le [linear_ordered_field α] {m n : ℚ} : (m : α) ≤ n ↔ m ≤ n :=
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ ┴
230 by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
id └────────┘ └──────┘ └─────────┘ └────────┘
src └────┘└────────┘└──┘└──────┘└┘└─────────┘└┘└────────┘└─
typ └────┘└────────┘└──┘└──────┘└┘└─────────┘└┘└────────┘└─
doc └────┘ └──┘ └┘ └┘ └─
txt └────┘ └──┘ └┘ └┘ └─
par └────┘ └──┘ └┘ └┘ └─
pid └──┘ └──┘ └┘ └┘ ┴└
st └───────────────┘└──────────┘└───────────┘└──────────┘┴└
231
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
232 @[simp, elim_cast] theorem cast_lt [linear_ordered_field α] {m n : ℚ} : (m : α) < n ↔ m < n :=
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ ┴
233 by simpa [-cast_le] using not_congr (@cast_le α _ n m)
id └───────┘ └─────┘ ┴ ┴ ┴
src └─────────────────────┘└───────┘┴ └─────┘┴ └─┘ ┴ └─
typ └─────────────────────┘└───────┘┴ └─────┘┴┴└─┘┴┴┴└─
doc └─────────────────────┘ ┴ ┴ └─┘ ┴ └─
txt └─────────────────────┘ ┴ ┴ └─┘ ┴ └─
par └─────────────────────┘ ┴ ┴ └─┘ ┴ └─
pid ┴└────────┘┴└────┘ ┴ ┴ └─┘ ┴ ┴└
st └────────────────────────────────────────────────────
234
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
235 @[simp] theorem cast_nonpos [linear_ordered_field α] {n : ℚ} : (n : α) ≤ 0 ↔ n ≤ 0 :=
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
236 by rw [← cast_zero, cast_le]
id └───────┘ └─────┘
src └────┘└───────┘└┘└─────┘└─
typ └────┘└───────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └──────────────┘└───────┘┴└
237
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
238 @[simp] theorem cast_pos [linear_ordered_field α] {n : ℚ} : (0 : α) < n ↔ 0 < n :=
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
239 by rw [← cast_zero, cast_lt]
id └───────┘ └─────┘
src └────┘└───────┘└┘└─────┘└─
typ └────┘└───────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └──────────────┘└───────┘┴└
240
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
241 @[simp] theorem cast_lt_zero [linear_ordered_field α] {n : ℚ} : (n : α) < 0 ↔ n < 0 :=
id └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────┘ ┴ ┴ ┴ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
242 by rw [← cast_zero, cast_lt]
id └───────┘ └─────┘
src └────┘└───────┘└┘└─────┘└─
typ └────┘└───────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └──────────────┘└───────┘┴└
243
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
244 @[simp, squash_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
id ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ └─────────┘ ┴
245 | ⟨n, d, h, c⟩ := show (n / (d : ℤ) : ℚ) = _, by rw [num_denom', mk_eq_div]
id ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └───────┘
src ┴ ┴ ┴ ┴ └──┘└────────┘└┘└───────┘└─
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└────────┘└┘└───────┘└─
doc ┴ └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└─────────┘┴└
246
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
247 @[simp, move_cast] theorem cast_min [discrete_linear_ordered_field α] {a b : ℚ} :
id └───────────────────────────┘ ┴ ┴
src └───────────────────────────┘ ┴
typ └───────────────────────────┘ ┴ ┴
doc └──┘ └───────┘ ┴
248 (↑(min a b) : α) = min a b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
249 by by_cases a ≤ b; simp [h, min]
id ┴ ┴ ┴ ┴ └─┘
src └───────┘ ┴┴┴ └────┘ └┘└─┘└─
typ └───────┘┴┴┴┴┴ └────┘┴└┘└─┘└─
doc └───────┘ ┴ ┴ └────┘ └┘ └─
txt └───────┘ ┴ ┴ └────┘ └┘ └─
par └───────┘ ┴ ┴ └────┘ └┘ └─
pid ┴ ┴ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────
250
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
251 @[simp, move_cast] theorem cast_max [discrete_linear_ordered_field α] {a b : ℚ} :
id └───────────────────────────┘ ┴ ┴
src └───────────────────────────┘ ┴
typ └───────────────────────────┘ ┴ ┴
doc └──┘ └───────┘ ┴
252 (↑(max a b) : α) = max a b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
253 by by_cases a ≤ b; simp [h, max]
id ┴ ┴ ┴ ┴ └─┘
src └───────┘ ┴┴┴ └────┘ └┘└─┘└─
typ └───────┘┴┴┴┴┴ └────┘┴└┘└─┘└─
doc └───────┘ ┴ ┴ └────┘ └┘ └─
txt └───────┘ ┴ ┴ └────┘ └┘ └─
par └───────┘ ┴ ┴ └────┘ └┘ └─
pid ┴ ┴ ┴ ┴┴ └┘ ┴└
st └──────────────────────────────
254
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
255 @[simp, move_cast] theorem cast_abs [discrete_linear_ordered_field α] {q : ℚ} :
id └───────────────────────────┘ ┴ ┴
src └───────────────────────────┘ ┴
typ └───────────────────────────┘ ┴ ┴
doc └──┘ └───────┘ ┴
256 ((abs q : ℚ) : α) = abs q :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc ┴
257 by simp [abs]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
258
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
259 end rat